$\forall$$A$, $T$:Type, $B$:(Id$\rightarrow$Type), $s$:$A$, $v$:$T$, ${\it tgf}$:(${\it tg}$:Id$\times$($A$$\rightarrow$$T$$\rightarrow$($B$(${\it tg}$) List))).
\\[0ex]sends{-}msgs($s$;$v$;${\it tgf}$) $\in$ (${\it tg}$:Id$\times$$B$(${\it tg}$)) List